A,B:es_realizer{i:l}.
R-sub{i:l}(A; B)  (es:event_system{i:l}. R-consistent(B; es)  R-consistent(A; es)) 

latex

Definitions	P  Q, True, R-consistent(R; es), ge(i; j), False, A, A  B, guard(T), sq_type(T), prop{i:l}, t  T, P  Q, x:A. B(x), , P  Q, ff, tt, P  Q, if b then t else f fi , Y, , R-sub{i:l}(A; B)
Lemmas	Rplus-right wf, Rplus-left wf, Rplus-implies, R-size-decreases, Rplus? wf, Rnone?-implies, ge wf, nat properties, assert of bnot, eqff to assert, not wf, bnot wf, assert wf, iff transitivity, eqtt to assert, bool wf, bool sq, Rnone? wf, bool cases, es realizer wf, nat plus wf, le wf, R-sub wf, event system wf, R-consistent wf, R-size wf, nat wf